<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Records: Adding Records to STLC</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Records<span class="subtitle">Adding Records to STLC</span></h1>


<div class="code">

<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing,-deprecated-hint-without-locality".<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#"><span class="id" title="library">Strings.String</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Maps</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Smallstep.html#"><span class="id" title="library">Smallstep</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Stlc.html#"><span class="id" title="library">Stlc</span></a>.<br/>
</div>

<div class="doc">
<a id="lab366"></a><h1 class="section">Adding Records</h1>

<div class="paragraph"> </div>

 We saw in chapter <a href="MoreStlc.html"><span class="inlineref">MoreStlc</span></a> how records can be treated as just
    syntactic sugar for nested uses of products.  This is OK for
    simple examples, but the encoding is informal (in reality, if we
    actually treated records this way, it would be carried out in the
    parser, which we are eliding here), and anyway it is not very
    efficient.  So it is also interesting to see how records can be
    treated as first-class citizens of the language.  This chapter
    shows how.

<div class="paragraph"> </div>

    Recall the informal definitions we gave before: 
<div class="paragraph"> </div>


<div class="paragraph"> </div>

    Syntax:
&lt;{
       t <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>                          Terms:
           | {i=t, ..., i=t}             record
           | t.i                         projection
           | ...

<div class="paragraph"> </div>

       v <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>                          Values:
           | {i=v, ..., i=v}             record value
           | ...

<div class="paragraph"> </div>

       T <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>                          Types:
           | {i:T, ..., i:T}             record type
           | ...
}&gt;
   Reduction:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">ti ==> ti'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Rcd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{i<sub>1</sub>=v<sub>1</sub>, ..., im=vm, in=tn, ...} ==> {i<sub>1</sub>=v<sub>1</sub>, ..., im=vm, in=tn', ...}</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub> ==> t<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_Proj1) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">t<sub>1</sub>.i ==> t<sub>1</sub>'.i</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ST_ProjRcd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">{..., i=vi, ...}.i ==> vi</td>
  <td></td>
</td>
</table></center>   Typing:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>1</sub> : T<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;...&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Gamma &#x22A2; tn : Tn</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Rcd) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; {i<sub>1</sub>=t<sub>1</sub>, ..., in=tn} : {i<sub>1</sub>:T<sub>1</sub>, ..., in:Tn}</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>0</sub> : {..., i:Ti, ...}</td>
  <td class="infrulenamecol" rowspan="3">
    (T_Proj) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">Gamma &#x22A2; t<sub>0</sub>.i : Ti</td>
  <td></td>
</td>
</table></center>
</div>

<div class="doc">
<a id="lab367"></a><h1 class="section">Formalizing Records</h1>

</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="STLCExtendedRecords" class="idref" href="#STLCExtendedRecords"><span class="id" title="module">STLCExtendedRecords</span></a>.<br/>
</div>

<div class="doc">
<a id="lab368"></a><h3 class="section">Syntax and Operational Semantics</h3>

<div class="paragraph"> </div>

 The most obvious way to formalize the syntax of record types would
    be this: 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="STLCExtendedRecords.FirstTry" class="idref" href="#STLCExtendedRecords.FirstTry"><span class="id" title="module">FirstTry</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="STLCExtendedRecords.FirstTry.alist" class="idref" href="#STLCExtendedRecords.FirstTry.alist"><span class="id" title="definition">alist</span></a> (<a id="X:1" class="idref" href="#X:1"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Records.html#X:1"><span class="id" title="variable">X</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.FirstTry.ty" class="idref" href="#STLCExtendedRecords.FirstTry.ty"><span class="id" title="inductive">ty</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.FirstTry.Base" class="idref" href="#STLCExtendedRecords.FirstTry.Base"><span class="id" title="constructor">Base</span></a>     : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:2"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.FirstTry.Arrow" class="idref" href="#STLCExtendedRecords.FirstTry.Arrow"><span class="id" title="constructor">Arrow</span></a>    : <a class="idref" href="Records.html#ty:2"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:2"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:2"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.FirstTry.TRcd" class="idref" href="#STLCExtendedRecords.FirstTry.TRcd"><span class="id" title="constructor">TRcd</span></a>     : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#STLCExtendedRecords.FirstTry.alist"><span class="id" title="definition">alist</span></a> <a class="idref" href="Records.html#ty:2"><span class="id" title="inductive">ty</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:2"><span class="id" title="inductive">ty</span></a>.<br/>
</div>

<div class="doc">
Unfortunately, we encounter here a limitation in Coq: this type
    does not automatically give us the induction principle we expect:
    the induction hypothesis in the <span class="inlinecode"><span class="id" title="var">TRcd</span></span> case doesn't give us
    any information about the <span class="inlinecode"><span class="id" title="var">ty</span></span> elements of the list, making it
    useless for the proofs we want to do.  
</div>
<div class="code">

<span class="comment">(*&nbsp;Check&nbsp;ty_ind.<br/>
&nbsp;&nbsp;&nbsp;====&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;ty_ind&nbsp;:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;P&nbsp;:&nbsp;ty&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Prop,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forall&nbsp;i&nbsp;:&nbsp;id,&nbsp;P&nbsp;(Base&nbsp;i))&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forall&nbsp;t&nbsp;:&nbsp;ty,&nbsp;P&nbsp;t&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;forall&nbsp;t<sub>0</sub>&nbsp;:&nbsp;ty,&nbsp;P&nbsp;t<sub>0</sub><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;P&nbsp;(Arrow&nbsp;t&nbsp;t<sub>0</sub>))&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(forall&nbsp;a&nbsp;:&nbsp;alist&nbsp;ty,&nbsp;P&nbsp;(TRcd&nbsp;a))&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;???&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;forall&nbsp;t&nbsp;:&nbsp;ty,&nbsp;P&nbsp;t<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="Records.html#STLCExtendedRecords.FirstTry"><span class="id" title="module">FirstTry</span></a>.<br/>
</div>

<div class="doc">
It is possible to get a better induction principle out of Coq, but
    the details of how this is done are not very pretty, and the
    principle we obtain is not as intuitive to use as the ones Coq
    generates automatically for simple <span class="inlinecode"><span class="id" title="keyword">Inductive</span></span> definitions.

<div class="paragraph"> </div>

    Fortunately, there is a different way of formalizing records that
    is, in some ways, even simpler and more natural: instead of using
    the standard Coq <span class="inlinecode"><span class="id" title="var">list</span></span> type, we can essentially incorporate its
    constructors ("nil" and "cons") in the syntax of our types. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.ty" class="idref" href="#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.Ty_Base" class="idref" href="#STLCExtendedRecords.Ty_Base"><span class="id" title="constructor">Ty_Base</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.Ty_Arrow" class="idref" href="#STLCExtendedRecords.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> : <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.Ty_RNil" class="idref" href="#STLCExtendedRecords.Ty_RNil"><span class="id" title="constructor">Ty_RNil</span></a> : <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.Ty_RCons" class="idref" href="#STLCExtendedRecords.Ty_RCons"><span class="id" title="constructor">Ty_RCons</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#ty:4"><span class="id" title="inductive">ty</span></a>.<br/>
</div>

<div class="doc">
Similarly, at the level of terms, we have constructors <span class="inlinecode"><span class="id" title="var">trnil</span></span>,
    for the empty record, and <span class="inlinecode"><span class="id" title="var">rcons</span></span>, which adds a single field to
    the front of a list of fields. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.tm" class="idref" href="#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.tm_var" class="idref" href="#STLCExtendedRecords.tm_var"><span class="id" title="constructor">tm_var</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.tm_app" class="idref" href="#STLCExtendedRecords.tm_app"><span class="id" title="constructor">tm_app</span></a> : <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.tm_abs" class="idref" href="#STLCExtendedRecords.tm_abs"><span class="id" title="constructor">tm_abs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;records&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.tm_rproj" class="idref" href="#STLCExtendedRecords.tm_rproj"><span class="id" title="constructor">tm_rproj</span></a> : <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.tm_rnil" class="idref" href="#STLCExtendedRecords.tm_rnil"><span class="id" title="constructor">tm_rnil</span></a> :  <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.tm_rcons" class="idref" href="#STLCExtendedRecords.tm_rcons"><span class="id" title="constructor">tm_rcons</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#tm:6"><span class="id" title="inductive">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="var">Declare</span> <span class="id" title="var">Custom</span> <span class="id" title="var">Entry</span> <span class="id" title="var">stlc_ty</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="578583e5bab5b75c1f745f27b2fa3362" class="idref" href="#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&quot;</span></a>&lt;{ e }&gt;" := <span class="id" title="var">e</span> (<span class="id" title="var">e</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="9117ef97be47c16687a336570867da4a" class="idref" href="#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&quot;</span></a>&lt;<span style='letter-spacing:-.4em;'>{</span>{ e <span style='letter-spacing:-.4em;'>}</span>}&gt;" := <span class="id" title="var">e</span> (<span class="id" title="var">e</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="6a63f178ee59cb86a0e9a58cfa031423" class="idref" href="#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">&quot;</span></a>( x )" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="d7100e6eff6251cc5929eb578deead9a" class="idref" href="#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">&quot;</span></a>( x )" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span>, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc::x" class="idref" href="#STLCExtendedRecords.:stlc::x"><span class="id" title="notation">&quot;</span></a>x" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc_ty::x" class="idref" href="#STLCExtendedRecords.:stlc_ty::x"><span class="id" title="notation">&quot;</span></a>x" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x" class="idref" href="#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">&quot;</span></a>S <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> T" := (<a class="idref" href="Records.html#STLCExtendedRecords.Ty_Arrow"><span class="id" title="constructor">Ty_Arrow</span></a> <span class="id" title="var">S</span> <span class="id" title="var">T</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc::x_x" class="idref" href="#STLCExtendedRecords.:stlc::x_x"><span class="id" title="notation">&quot;</span></a>x y" := (<a class="idref" href="Records.html#STLCExtendedRecords.tm_app"><span class="id" title="constructor">tm_app</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>" class="idref" href="#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">&quot;</span></a>\ x : t , y" :=<br/>
&nbsp;&nbsp;(<a class="idref" href="Records.html#STLCExtendedRecords.tm_abs"><span class="id" title="constructor">tm_abs</span></a> <span class="id" title="var">x</span> <span class="id" title="var">t</span> <span class="id" title="var">y</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">y</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Coercion</span> <a class="idref" href="Records.html#STLCExtendedRecords.tm_var"><span class="id" title="constructor">tm_var</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.tm_var"><span class="id" title="constructor">:</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.tm_var"><span class="id" title="constructor">string</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.tm_var"><span class="id" title="constructor">&gt;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.tm_var"><span class="id" title="constructor">tm</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="f2dea8078f7ea8fe55302018486eb6d<sub>9</sub>" class="idref" href="#f2dea8078f7ea8fe55302018486eb6d<sub>9</sub>"><span class="id" title="notation">&quot;</span></a>{ x }" := <span class="id" title="var">x</span> (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 1, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc_ty::'Base'_x" class="idref" href="#STLCExtendedRecords.:stlc_ty::'Base'_x"><span class="id" title="notation">&quot;</span></a>'Base' x" := (<a class="idref" href="Records.html#STLCExtendedRecords.Ty_Base"><span class="id" title="constructor">Ty_Base</span></a> <span class="id" title="var">x</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x" class="idref" href="#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">&quot;</span></a>  l ':' t<sub>1</sub>  '::' t<sub>2</sub>" := (<a class="idref" href="Records.html#STLCExtendedRecords.Ty_RCons"><span class="id" title="constructor">Ty_RCons</span></a> <span class="id" title="var">l</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="81f41eb8d6c9df1b60000d935db1438c" class="idref" href="#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">&quot;</span></a> l := e<sub>1</sub> '::' e<sub>2</sub>" := (<a class="idref" href="Records.html#STLCExtendedRecords.tm_rcons"><span class="id" title="constructor">tm_rcons</span></a> <span class="id" title="var">l</span> <span class="id" title="var">e<sub>1</sub></span> <span class="id" title="var">e<sub>2</sub></span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc_ty::'nil'" class="idref" href="#STLCExtendedRecords.:stlc_ty::'nil'"><span class="id" title="notation">&quot;</span></a>'nil'" := (<a class="idref" href="Records.html#STLCExtendedRecords.Ty_RNil"><span class="id" title="constructor">Ty_RNil</span></a>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc::'nil'" class="idref" href="#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">&quot;</span></a>'nil'" := (<a class="idref" href="Records.html#STLCExtendedRecords.tm_rnil"><span class="id" title="constructor">tm_rnil</span></a>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>).<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.:stlc::x_'--&gt;'_x" class="idref" href="#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation">&quot;</span></a>o <span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> l" := (<a class="idref" href="Records.html#STLCExtendedRecords.tm_rproj"><span class="id" title="constructor">tm_rproj</span></a> <span class="id" title="var">o</span> <span class="id" title="var">l</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/>
</div>

<div class="doc">
Some examples... 
</div>
<div class="code">
<span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">string_scope</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.a" class="idref" href="#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> := "a".<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.f" class="idref" href="#STLCExtendedRecords.f"><span class="id" title="abbreviation">f</span></a> := "f".<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.g" class="idref" href="#STLCExtendedRecords.g"><span class="id" title="abbreviation">g</span></a> := "g".<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.l" class="idref" href="#STLCExtendedRecords.l"><span class="id" title="abbreviation">l</span></a> := "l".<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.A" class="idref" href="#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a> := <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'Base'_x"><span class="id" title="notation">Base</span></a> "A" <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.B" class="idref" href="#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a> := <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'Base'_x"><span class="id" title="notation">Base</span></a> "B" <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>.<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.k" class="idref" href="#STLCExtendedRecords.k"><span class="id" title="abbreviation">k</span></a> := "k".<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.i1" class="idref" href="#STLCExtendedRecords.i1"><span class="id" title="abbreviation">i<sub>1</sub></span></a> := "i<sub>1</sub>".<br/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.i2" class="idref" href="#STLCExtendedRecords.i2"><span class="id" title="abbreviation">i<sub>2</sub></span></a> := "i<sub>2</sub>".<br/>
</div>

<div class="doc">
<span class="inlinecode">{</span> <span class="inlinecode"><span class="id" title="var">i<sub>1</sub></span>:<span class="id" title="var">A</span></span> <span class="inlinecode">}</span> 
</div>
<div class="code">

<span class="comment">(*&nbsp;Check&nbsp;(RCons&nbsp;i<sub>1</sub>&nbsp;A&nbsp;RNil).&nbsp;*)</span><br/>
</div>

<div class="doc">
<span class="inlinecode">{</span> <span class="inlinecode"><span class="id" title="var">i<sub>1</sub></span>:<span class="id" title="var">A</span>→<span class="id" title="var">B</span>,</span> <span class="inlinecode"><span class="id" title="var">i<sub>2</sub></span>:<span class="id" title="var">A</span></span> <span class="inlinecode">}</span> 
</div>
<div class="code">

<span class="comment">(*&nbsp;Check&nbsp;(RCons&nbsp;i<sub>1</sub>&nbsp;(Arrow&nbsp;A&nbsp;B)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(RCons&nbsp;i<sub>2</sub>&nbsp;A&nbsp;RNil)).&nbsp;*)</span><br/>
</div>

<div class="doc">
<a id="lab369"></a><h3 class="section">Well-Formedness</h3>

<div class="paragraph"> </div>

 One issue with generalizing the abstract syntax for records from
    lists to the nil/cons presentation is that it introduces the
    possibility of writing strange types like this... 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="STLCExtendedRecords.weird_type" class="idref" href="#STLCExtendedRecords.weird_type"><span class="id" title="definition">weird_type</span></a> := <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a>  <a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a>  <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>.<br/>
</div>

<div class="doc">
where the "tail" of a record type is not actually a record type! 
<div class="paragraph"> </div>

 We'll structure our typing judgement so that no ill-formed types
    like <span class="inlinecode"><span class="id" title="var">weird_type</span></span> are ever assigned to terms.  To support this, we
    define predicates <span class="inlinecode"><span class="id" title="var">record_ty</span></span> and <span class="inlinecode"><span class="id" title="var">record_tm</span></span>, which identify
    record types and terms, and <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span> which rules out the
    ill-formed types. 
<div class="paragraph"> </div>

 First, a type is a record type if it is built with just <span class="inlinecode"><span class="id" title="var">RNil</span></span>
    and <span class="inlinecode"><span class="id" title="var">RCons</span></span> at the outermost level. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.record_ty" class="idref" href="#STLCExtendedRecords.record_ty"><span class="id" title="inductive">record_ty</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.RTnil" class="idref" href="#STLCExtendedRecords.RTnil"><span class="id" title="constructor">RTnil</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#record_ty:8"><span class="id" title="inductive">record_ty</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.RTcons" class="idref" href="#STLCExtendedRecords.RTcons"><span class="id" title="constructor">RTcons</span></a> : <span class="id" title="keyword">∀</span> <a id="i:10" class="idref" href="#i:10"><span class="id" title="binder">i</span></a> <a id="T<sub>1</sub>:11" class="idref" href="#T<sub>1</sub>:11"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:12" class="idref" href="#T<sub>2</sub>:12"><span class="id" title="binder">T<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#record_ty:8"><span class="id" title="inductive">record_ty</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#i:10"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#T<sub>1</sub>:11"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:12"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>.<br/>
</div>

<div class="doc">
With this, we can define well-formed types. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.well_formed_ty" class="idref" href="#STLCExtendedRecords.well_formed_ty"><span class="id" title="inductive">well_formed_ty</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.wfBase" class="idref" href="#STLCExtendedRecords.wfBase"><span class="id" title="constructor">wfBase</span></a> : <span class="id" title="keyword">∀</span> (<a id="i:15" class="idref" href="#i:15"><span class="id" title="binder">i</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'Base'_x"><span class="id" title="notation">Base</span></a> <a class="idref" href="Records.html#i:15"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.wfArrow" class="idref" href="#STLCExtendedRecords.wfArrow"><span class="id" title="constructor">wfArrow</span></a> : <span class="id" title="keyword">∀</span> <a id="T<sub>1</sub>:16" class="idref" href="#T<sub>1</sub>:16"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:17" class="idref" href="#T<sub>2</sub>:17"><span class="id" title="binder">T<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T<sub>1</sub>:16"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:17"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#T<sub>1</sub>:16"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:17"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.wfRNil" class="idref" href="#STLCExtendedRecords.wfRNil"><span class="id" title="constructor">wfRNil</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.wfRCons" class="idref" href="#STLCExtendedRecords.wfRCons"><span class="id" title="constructor">wfRCons</span></a> : <span class="id" title="keyword">∀</span> <a id="i:18" class="idref" href="#i:18"><span class="id" title="binder">i</span></a> <a id="T<sub>1</sub>:19" class="idref" href="#T<sub>1</sub>:19"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:20" class="idref" href="#T<sub>2</sub>:20"><span class="id" title="binder">T<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T<sub>1</sub>:19"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:20"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.record_ty"><span class="id" title="inductive">record_ty</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:20"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#well_formed_ty:13"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <a class="idref" href="Records.html#i:18"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#T<sub>1</sub>:19"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:20"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Records.html#record_ty"><span class="id" title="inductive">record_ty</span></a> <a class="idref" href="Records.html#well_formed_ty"><span class="id" title="inductive">well_formed_ty</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
Note that <span class="inlinecode"><span class="id" title="var">record_ty</span></span> is not recursive -- it just checks the
    outermost constructor.  The <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span> property, on the
    other hand, verifies that the whole type is well formed in the
    sense that the tail of every record (the second argument to
    <span class="inlinecode"><span class="id" title="var">RCons</span></span>) is a record.

<div class="paragraph"> </div>

    Of course, we should also be concerned about ill-formed terms, not
    just types; but typechecking can rule those out without the help
    of an extra <span class="inlinecode"><span class="id" title="var">well_formed_tm</span></span> definition because it already
    examines the structure of terms.  All we need is an analog of
    <span class="inlinecode"><span class="id" title="var">record_ty</span></span> saying that a term is a record term if it is built
    with <span class="inlinecode"><span class="id" title="var">trnil</span></span> and <span class="inlinecode"><span class="id" title="var">rcons</span></span>. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.record_tm" class="idref" href="#STLCExtendedRecords.record_tm"><span class="id" title="inductive">record_tm</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.rtnil" class="idref" href="#STLCExtendedRecords.rtnil"><span class="id" title="constructor">rtnil</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#record_tm:21"><span class="id" title="inductive">record_tm</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.rtcons" class="idref" href="#STLCExtendedRecords.rtcons"><span class="id" title="constructor">rtcons</span></a> : <span class="id" title="keyword">∀</span> <a id="i:23" class="idref" href="#i:23"><span class="id" title="binder">i</span></a> <a id="t<sub>1</sub>:24" class="idref" href="#t<sub>1</sub>:24"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:25" class="idref" href="#t<sub>2</sub>:25"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#record_tm:21"><span class="id" title="inductive">record_tm</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#i:23"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#t<sub>1</sub>:24"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#t<sub>2</sub>:25"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Records.html#record_tm"><span class="id" title="inductive">record_tm</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
<a id="lab370"></a><h3 class="section">Substitution</h3>

<div class="paragraph"> </div>

 Substitution extends easily. 
</div>
<div class="code">

<span class="id" title="keyword">Reserved Notation</span> &quot;'[' x ':=' s ']' t" (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 20, <span class="id" title="var">x</span> <span class="id" title="keyword">constr</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="STLCExtendedRecords.subst" class="idref" href="#STLCExtendedRecords.subst"><span class="id" title="definition">subst</span></a> (<a id="x:26" class="idref" href="#x:26"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="s:27" class="idref" href="#s:27"><span class="id" title="binder">s</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a>) (<a id="t:28" class="idref" href="#t:28"><span class="id" title="binder">t</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Records.html#t:28"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#STLCExtendedRecords.tm_var"><span class="id" title="constructor">tm_var</span></a> <span class="id" title="var">y</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <span class="id" title="definition">eqb_string</span> <a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="keyword">then</span> <a class="idref" href="Records.html#s:27"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Records.html#t:28"><span class="id" title="variable">t</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><span class="id" title="var">y</span><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a><span class="id" title="var">T</span><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <span class="id" title="definition">eqb_string</span> <a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span> <span class="id" title="keyword">then</span> <a class="idref" href="Records.html#t:28"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><span class="id" title="var">y</span><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a><span class="id" title="var">T</span><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a><a class="idref" href="Records.html#s:27"><span class="id" title="variable">s</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a><a class="idref" href="Records.html#s:27"><span class="id" title="variable">s</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a><a class="idref" href="Records.html#s:27"><span class="id" title="variable">s</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <span class="id" title="var">i</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#s:27"><span class="id" title="variable">s</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <span class="id" title="var">i</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">i</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <span class="id" title="var">tr</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">i</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a>  <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#s:27"><span class="id" title="variable">s</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:26"><span class="id" title="variable">x</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#s:27"><span class="id" title="variable">s</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a> <span class="id" title="var">tr</span><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>" class="idref" href="#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">&quot;</span></a>'[' x ':=' s ']' t" := (<a class="idref" href="Records.html#subst:29"><span class="id" title="definition">subst</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span>) (<span class="id" title="keyword">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>).<br/>
</div>

<div class="doc">
<a id="lab371"></a><h3 class="section">Reduction</h3>

<div class="paragraph"> </div>

 A record is a value if all of its fields are. 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.value" class="idref" href="#STLCExtendedRecords.value"><span class="id" title="inductive">value</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.v_abs" class="idref" href="#STLCExtendedRecords.v_abs"><span class="id" title="constructor">v_abs</span></a> : <span class="id" title="keyword">∀</span> <a id="x:33" class="idref" href="#x:33"><span class="id" title="binder">x</span></a> <a id="T<sub>2</sub>:34" class="idref" href="#T<sub>2</sub>:34"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="t<sub>1</sub>:35" class="idref" href="#t<sub>1</sub>:35"><span class="id" title="binder">t<sub>1</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#value:31"><span class="id" title="inductive">value</span></a>  <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a> <a class="idref" href="Records.html#x:33"><span class="id" title="variable">x</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:34"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#t<sub>1</sub>:35"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.v_rnil" class="idref" href="#STLCExtendedRecords.v_rnil"><span class="id" title="constructor">v_rnil</span></a> : <a class="idref" href="Records.html#value:31"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.v_rcons" class="idref" href="#STLCExtendedRecords.v_rcons"><span class="id" title="constructor">v_rcons</span></a> : <span class="id" title="keyword">∀</span> <a id="i:36" class="idref" href="#i:36"><span class="id" title="binder">i</span></a> <a id="v<sub>1</sub>:37" class="idref" href="#v<sub>1</sub>:37"><span class="id" title="binder">v<sub>1</sub></span></a> <a id="vr:38" class="idref" href="#vr:38"><span class="id" title="binder">vr</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#value:31"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#v<sub>1</sub>:37"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#value:31"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#vr:38"><span class="id" title="variable">vr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#value:31"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#i:36"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#v<sub>1</sub>:37"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#vr:38"><span class="id" title="variable">vr</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Records.html#value"><span class="id" title="inductive">value</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
To define reduction, we'll need a utility function for extracting
    one field from record term: 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="STLCExtendedRecords.tlookup" class="idref" href="#STLCExtendedRecords.tlookup"><span class="id" title="definition">tlookup</span></a> (<a id="i:39" class="idref" href="#i:39"><span class="id" title="binder">i</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="tr:40" class="idref" href="#tr:40"><span class="id" title="binder">tr</span></a>:<a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Records.html#tr:40"><span class="id" title="variable">tr</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">i'</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <span class="id" title="var">t</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <span class="id" title="var">tr'</span><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> ⇒ <span class="id" title="keyword">if</span> <span class="id" title="definition">eqb_string</span> <a class="idref" href="Records.html#i:39"><span class="id" title="variable">i</span></a> <span class="id" title="var">i'</span> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">t</span> <span class="id" title="keyword">else</span> <a class="idref" href="Records.html#tlookup:41"><span class="id" title="definition">tlookup</span></a> <a class="idref" href="Records.html#i:39"><span class="id" title="variable">i</span></a> <span class="id" title="var">tr'</span><br/>
&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" title="var">step</span></span> function uses this term-level lookup function in the
    projection rule. 
</div>
<div class="code">

<span class="id" title="keyword">Reserved Notation</span> &quot;t '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t'" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.step" class="idref" href="#STLCExtendedRecords.step"><span class="id" title="inductive">step</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.ST_AppAbs" class="idref" href="#STLCExtendedRecords.ST_AppAbs"><span class="id" title="constructor">ST_AppAbs</span></a> : <span class="id" title="keyword">∀</span> <a id="x:45" class="idref" href="#x:45"><span class="id" title="binder">x</span></a> <a id="T<sub>2</sub>:46" class="idref" href="#T<sub>2</sub>:46"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="t<sub>1</sub>:47" class="idref" href="#t<sub>1</sub>:47"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="v<sub>2</sub>:48" class="idref" href="#v<sub>2</sub>:48"><span class="id" title="binder">v<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#v<sub>2</sub>:48"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#x:45"><span class="id" title="variable">x</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a><a class="idref" href="Records.html#T<sub>2</sub>:46"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#t<sub>1</sub>:47"><span class="id" title="variable">t<sub>1</sub></span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#v<sub>2</sub>:48"><span class="id" title="variable">v<sub>2</sub></span></a><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:45"><span class="id" title="variable">x</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a><a class="idref" href="Records.html#v<sub>2</sub>:48"><span class="id" title="variable">v<sub>2</sub></span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="Records.html#t<sub>1</sub>:47"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.ST_App1" class="idref" href="#STLCExtendedRecords.ST_App1"><span class="id" title="constructor">ST_App1</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:49" class="idref" href="#t<sub>1</sub>:49"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':50" class="idref" href="#t<sub>1</sub>':50"><span class="id" title="binder">t<sub>1</sub>'</span></a> <a id="t<sub>2</sub>:51" class="idref" href="#t<sub>2</sub>:51"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#t<sub>1</sub>:49"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#t<sub>1</sub>':50"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#t<sub>1</sub>:49"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#t<sub>2</sub>:51"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#t<sub>1</sub>':50"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="Records.html#t<sub>2</sub>:51"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.ST_App2" class="idref" href="#STLCExtendedRecords.ST_App2"><span class="id" title="constructor">ST_App2</span></a> : <span class="id" title="keyword">∀</span> <a id="v<sub>1</sub>:52" class="idref" href="#v<sub>1</sub>:52"><span class="id" title="binder">v<sub>1</sub></span></a> <a id="t<sub>2</sub>:53" class="idref" href="#t<sub>2</sub>:53"><span class="id" title="binder">t<sub>2</sub></span></a> <a id="t<sub>2</sub>':54" class="idref" href="#t<sub>2</sub>':54"><span class="id" title="binder">t<sub>2</sub>'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#v<sub>1</sub>:52"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#t<sub>2</sub>:53"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#t<sub>2</sub>':54"><span class="id" title="variable">t<sub>2</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#v<sub>1</sub>:52"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Records.html#t<sub>2</sub>:53"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Records.html#v<sub>1</sub>:52"><span class="id" title="variable">v<sub>1</sub></span></a>  <a class="idref" href="Records.html#t<sub>2</sub>':54"><span class="id" title="variable">t<sub>2</sub>'</span></a><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.ST_Proj1" class="idref" href="#STLCExtendedRecords.ST_Proj1"><span class="id" title="constructor">ST_Proj1</span></a> : <span class="id" title="keyword">∀</span> <a id="t<sub>1</sub>:55" class="idref" href="#t<sub>1</sub>:55"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':56" class="idref" href="#t<sub>1</sub>':56"><span class="id" title="binder">t<sub>1</sub>'</span></a> <a id="i:57" class="idref" href="#i:57"><span class="id" title="binder">i</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#t<sub>1</sub>:55"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#t<sub>1</sub>':56"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#t<sub>1</sub>:55"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#i:57"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#t<sub>1</sub>':56"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#i:57"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.ST_ProjRcd" class="idref" href="#STLCExtendedRecords.ST_ProjRcd"><span class="id" title="constructor">ST_ProjRcd</span></a> : <span class="id" title="keyword">∀</span> <a id="tr:58" class="idref" href="#tr:58"><span class="id" title="binder">tr</span></a> <a id="i:59" class="idref" href="#i:59"><span class="id" title="binder">i</span></a> <a id="vi:60" class="idref" href="#vi:60"><span class="id" title="binder">vi</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#tr:58"><span class="id" title="variable">tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.tlookup"><span class="id" title="definition">tlookup</span></a> <a class="idref" href="Records.html#i:59"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#tr:58"><span class="id" title="variable">tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Records.html#vi:60"><span class="id" title="variable">vi</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#tr:58"><span class="id" title="variable">tr</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#i:59"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#vi:60"><span class="id" title="variable">vi</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.ST_Rcd_Head" class="idref" href="#STLCExtendedRecords.ST_Rcd_Head"><span class="id" title="constructor">ST_Rcd_Head</span></a> : <span class="id" title="keyword">∀</span> <a id="i:61" class="idref" href="#i:61"><span class="id" title="binder">i</span></a> <a id="t<sub>1</sub>:62" class="idref" href="#t<sub>1</sub>:62"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>1</sub>':63" class="idref" href="#t<sub>1</sub>':63"><span class="id" title="binder">t<sub>1</sub>'</span></a> <a id="tr<sub>2</sub>:64" class="idref" href="#tr<sub>2</sub>:64"><span class="id" title="binder">tr<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#t<sub>1</sub>:62"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#t<sub>1</sub>':63"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#i:61"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#t<sub>1</sub>:62"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#tr<sub>2</sub>:64"><span class="id" title="variable">tr<sub>2</sub></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#i:61"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#t<sub>1</sub>':63"><span class="id" title="variable">t<sub>1</sub>'</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#tr<sub>2</sub>:64"><span class="id" title="variable">tr<sub>2</sub></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.ST_Rcd_Tail" class="idref" href="#STLCExtendedRecords.ST_Rcd_Tail"><span class="id" title="constructor">ST_Rcd_Tail</span></a> : <span class="id" title="keyword">∀</span> <a id="i:65" class="idref" href="#i:65"><span class="id" title="binder">i</span></a> <a id="v<sub>1</sub>:66" class="idref" href="#v<sub>1</sub>:66"><span class="id" title="binder">v<sub>1</sub></span></a> <a id="tr<sub>2</sub>:67" class="idref" href="#tr<sub>2</sub>:67"><span class="id" title="binder">tr<sub>2</sub></span></a> <a id="tr<sub>2</sub>':68" class="idref" href="#tr<sub>2</sub>':68"><span class="id" title="binder">tr<sub>2</sub>'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#v<sub>1</sub>:66"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#tr<sub>2</sub>:67"><span class="id" title="variable">tr<sub>2</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#tr<sub>2</sub>':68"><span class="id" title="variable">tr<sub>2</sub>'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#i:65"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#v<sub>1</sub>:66"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#tr<sub>2</sub>:67"><span class="id" title="variable">tr<sub>2</sub></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#i:65"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#v<sub>1</sub>:66"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#tr<sub>2</sub>':68"><span class="id" title="variable">tr<sub>2</sub>'</span></a> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="STLCExtendedRecords.:::x_'--&gt;'_x" class="idref" href="#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation">&quot;</span></a>t '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' t'" := (<a class="idref" href="Records.html#step:44"><span class="id" title="inductive">step</span></a> <span class="id" title="var">t</span> <span class="id" title="var">t'</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="STLCExtendedRecords.multistep" class="idref" href="#STLCExtendedRecords.multistep"><span class="id" title="abbreviation">multistep</span></a> := (<a class="idref" href="Smallstep.html#multi"><span class="id" title="inductive">multi</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.step"><span class="id" title="inductive">step</span></a>).<br/>
<span class="id" title="keyword">Notation</span> <a id="2533d5c9adea6de7e4d0d5ee86b41598" class="idref" href="#2533d5c9adea6de7e4d0d5ee86b41598"><span class="id" title="notation">&quot;</span></a>t<sub>1</sub> '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span><span style='letter-spacing:-.2em;'>&gt;</span><span style='vertical-align:15%;'>*</span></span></span>' t<sub>2</sub>" := (<a class="idref" href="Records.html#STLCExtendedRecords.multistep"><span class="id" title="abbreviation">multistep</span></a> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Records.html#step"><span class="id" title="inductive">step</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
<a id="lab372"></a><h3 class="section">Typing</h3>

<div class="paragraph"> </div>

 Next we define the typing rules.  These are nearly direct
    transcriptions of the inference rules shown above: the only
    significant difference is the use of <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span>.  In the
    informal presentation we used a grammar that only allowed
    well-formed record types, so we didn't have to add a separate
    check.

<div class="paragraph"> </div>

    One sanity condition that we'd like to maintain is that, whenever
    <span class="inlinecode"><span class="id" title="var">has_type</span></span> <span class="inlinecode"><span class="id" title="var">Gamma</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> holds, will also be the case that
    <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span>, so that <span class="inlinecode"><span class="id" title="var">has_type</span></span> never assigns ill-formed
    types to terms.  In fact, we prove this theorem below.  However,
    we don't want to clutter the definition of <span class="inlinecode"><span class="id" title="var">has_type</span></span> with
    unnecessary uses of <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span>.  Instead, we place
    <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span> checks only where needed: where an inductive call
    to <span class="inlinecode"><span class="id" title="var">has_type</span></span> won't already be checking the well-formedness of a
    type.  For example, we check <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> in the <span class="inlinecode"><span class="id" title="var">T_Var</span></span>
    case, because there is no inductive <span class="inlinecode"><span class="id" title="var">has_type</span></span> call that would
    enforce this.  Similarly, in the <span class="inlinecode"><span class="id" title="var">T_Abs</span></span> case, we require a proof
    of <span class="inlinecode"><span class="id" title="var">well_formed_ty</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>11</sub></span></span> because the inductive call to <span class="inlinecode"><span class="id" title="var">has_type</span></span>
    only guarantees that <span class="inlinecode"><span class="id" title="var">T<sub>12</sub></span></span> is well-formed. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="STLCExtendedRecords.Tlookup" class="idref" href="#STLCExtendedRecords.Tlookup"><span class="id" title="definition">Tlookup</span></a> (<a id="i:69" class="idref" href="#i:69"><span class="id" title="binder">i</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<a id="Tr:70" class="idref" href="#Tr:70"><span class="id" title="binder">Tr</span></a>:<a class="idref" href="Records.html#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Records.html#Tr:70"><span class="id" title="variable">Tr</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a> <span class="id" title="var">i'</span> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <span class="id" title="var">T</span> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">Tr'</span> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <span class="id" title="definition">eqb_string</span> <a class="idref" href="Records.html#i:69"><span class="id" title="variable">i</span></a> <span class="id" title="var">i'</span> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> <span class="id" title="keyword">else</span> <a class="idref" href="Records.html#Tlookup:71"><span class="id" title="definition">Tlookup</span></a> <a class="idref" href="Records.html#i:69"><span class="id" title="variable">i</span></a> <span class="id" title="var">Tr'</span><br/>
&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="STLCExtendedRecords.context" class="idref" href="#STLCExtendedRecords.context"><span class="id" title="definition">context</span></a> := <span class="id" title="definition">partial_map</span> <a class="idref" href="Records.html#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Reserved Notation</span> &quot;Gamma '&#x22A2;' t '&#x2208;' T" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 40,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">t</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc</span>, <span class="id" title="var">T</span> <span class="id" title="var">custom</span> <span class="id" title="var">stlc_ty</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="STLCExtendedRecords.has_type" class="idref" href="#STLCExtendedRecords.has_type"><span class="id" title="inductive">has_type</span></a> (<a id="Gamma:73" class="idref" href="#Gamma:73"><span class="id" title="binder">Gamma</span></a> : <a class="idref" href="Records.html#STLCExtendedRecords.context"><span class="id" title="definition">context</span></a>) :<a class="idref" href="Records.html#STLCExtendedRecords.tm"><span class="id" title="inductive">tm</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.ty"><span class="id" title="inductive">ty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.T_Var" class="idref" href="#STLCExtendedRecords.T_Var"><span class="id" title="constructor">T_Var</span></a> : <span class="id" title="keyword">∀</span> <a id="x:76" class="idref" href="#x:76"><span class="id" title="binder">x</span></a> <a id="T:77" class="idref" href="#T:77"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#x:76"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Records.html#T:77"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.well_formed_ty"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T:77"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#x:76"><span class="id" title="variable">x</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:77"><span class="id" title="variable">T</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.T_Abs" class="idref" href="#STLCExtendedRecords.T_Abs"><span class="id" title="constructor">T_Abs</span></a> : <span class="id" title="keyword">∀</span> <a id="x:78" class="idref" href="#x:78"><span class="id" title="binder">x</span></a> <a id="T<sub>11</sub>:79" class="idref" href="#T<sub>11</sub>:79"><span class="id" title="binder">T<sub>11</sub></span></a> <a id="T<sub>12</sub>:80" class="idref" href="#T<sub>12</sub>:80"><span class="id" title="binder">T<sub>12</sub></span></a> <a id="t<sub>12</sub>:81" class="idref" href="#t<sub>12</sub>:81"><span class="id" title="binder">t<sub>12</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.well_formed_ty"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T<sub>11</sub>:79"><span class="id" title="variable">T<sub>11</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#x:78"><span class="id" title="variable">x</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="Records.html#T<sub>11</sub>:79"><span class="id" title="variable">T<sub>11</sub></span></a><span class="id" title="notation">;</span> <a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t<sub>12</sub>:81"><span class="id" title="variable">t<sub>12</sub></span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T<sub>12</sub>:80"><span class="id" title="variable">T<sub>12</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#x:78"><span class="id" title="variable">x</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#T<sub>11</sub>:79"><span class="id" title="variable">T<sub>11</sub></span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#t<sub>12</sub>:81"><span class="id" title="variable">t<sub>12</sub></span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#T<sub>11</sub>:79"><span class="id" title="variable">T<sub>11</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#T<sub>12</sub>:80"><span class="id" title="variable">T<sub>12</sub></span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.T_App" class="idref" href="#STLCExtendedRecords.T_App"><span class="id" title="constructor">T_App</span></a> : <span class="id" title="keyword">∀</span> <a id="T<sub>1</sub>:82" class="idref" href="#T<sub>1</sub>:82"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:83" class="idref" href="#T<sub>2</sub>:83"><span class="id" title="binder">T<sub>2</sub></span></a> <a id="t<sub>1</sub>:84" class="idref" href="#t<sub>1</sub>:84"><span class="id" title="binder">t<sub>1</sub></span></a> <a id="t<sub>2</sub>:85" class="idref" href="#t<sub>2</sub>:85"><span class="id" title="binder">t<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t<sub>1</sub>:84"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#T<sub>1</sub>:82"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:83"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t<sub>2</sub>:85"><span class="id" title="variable">t<sub>2</sub></span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T<sub>1</sub>:82"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#t<sub>1</sub>:84"><span class="id" title="variable">t<sub>1</sub></span></a> <a class="idref" href="Records.html#t<sub>2</sub>:85"><span class="id" title="variable">t<sub>2</sub></span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T<sub>2</sub>:83"><span class="id" title="variable">T<sub>2</sub></span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;records:&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.T_Proj" class="idref" href="#STLCExtendedRecords.T_Proj"><span class="id" title="constructor">T_Proj</span></a> : <span class="id" title="keyword">∀</span> <a id="i:86" class="idref" href="#i:86"><span class="id" title="binder">i</span></a> <a id="t:87" class="idref" href="#t:87"><span class="id" title="binder">t</span></a> <a id="Ti:88" class="idref" href="#Ti:88"><span class="id" title="binder">Ti</span></a> <a id="Tr:89" class="idref" href="#Tr:89"><span class="id" title="binder">Tr</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:87"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#Tr:89"><span class="id" title="variable">Tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.Tlookup"><span class="id" title="definition">Tlookup</span></a> <a class="idref" href="Records.html#i:86"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#Tr:89"><span class="id" title="variable">Tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Records.html#Ti:88"><span class="id" title="variable">Ti</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#t:87"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#i:86"><span class="id" title="variable">i</span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#Ti:88"><span class="id" title="variable">Ti</span></a><br/>
&nbsp;| <a id="STLCExtendedRecords.T_RNil" class="idref" href="#STLCExtendedRecords.T_RNil"><span class="id" title="constructor">T_RNil</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'nil'"><span class="id" title="notation">nil</span></a><br/>
&nbsp;&nbsp;| <a id="STLCExtendedRecords.T_RCons" class="idref" href="#STLCExtendedRecords.T_RCons"><span class="id" title="constructor">T_RCons</span></a> : <span class="id" title="keyword">∀</span> <a id="i:90" class="idref" href="#i:90"><span class="id" title="binder">i</span></a> <a id="t:91" class="idref" href="#t:91"><span class="id" title="binder">t</span></a> <a id="T:92" class="idref" href="#T:92"><span class="id" title="binder">T</span></a> <a id="tr:93" class="idref" href="#tr:93"><span class="id" title="binder">tr</span></a> <a id="Tr:94" class="idref" href="#Tr:94"><span class="id" title="binder">Tr</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:91"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:92"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#tr:93"><span class="id" title="variable">tr</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#Tr:94"><span class="id" title="variable">Tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.record_ty"><span class="id" title="inductive">record_ty</span></a> <a class="idref" href="Records.html#Tr:94"><span class="id" title="variable">Tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.record_tm"><span class="id" title="inductive">record_tm</span></a> <a class="idref" href="Records.html#tr:93"><span class="id" title="variable">tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:73"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#i:90"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#t:91"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#tr:93"><span class="id" title="variable">tr</span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#i:90"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#T:92"><span class="id" title="variable">T</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#Tr:94"><span class="id" title="variable">Tr</span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a><br/>
<br/>
<span class="id" title="keyword">where</span> <a id="308929c34b30aea3b8569a5808139a<sub>21</sub>" class="idref" href="#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&quot;</span></a>Gamma '&#x22A2;' t '&#x2208;' T" := (<a class="idref" href="Records.html#has_type:75"><span class="id" title="inductive">has_type</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Hint Constructors</span> <a class="idref" href="Records.html#has_type"><span class="id" title="inductive">has_type</span></a> : <span class="id" title="var">core</span>.<br/>
</div>

<div class="doc">
<a id="lab373"></a><h2 class="section">Examples</h2>

<div class="paragraph"> </div>

<a id="lab374"></a><h4 class="section">Exercise: 2 stars, standard (examples)</h4>
 Finish the proofs below.  Feel free to use Coq's automation
    features in this proof.  However, if you are not confident about
    how the type system works, you may want to carry out the proofs
    first using the basic features (<span class="inlinecode"><span class="id" title="tactic">apply</span></span> instead of <span class="inlinecode"><span class="id" title="tactic">eapply</span></span>, in
    particular) and then perhaps compress it using automation.  Before
    starting to prove anything, make sure you understand what it is
    saying. 
</div>
<div class="code">

<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.typing_example_2" class="idref" href="#STLCExtendedRecords.typing_example_2"><span class="id" title="lemma">typing_example_2</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i1"><span class="id" title="abbreviation">i<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i2"><span class="id" title="abbreviation">i<sub>2</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'nil'"><span class="id" title="notation">nil</span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i2"><span class="id" title="abbreviation">i<sub>2</sub></span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i1"><span class="id" title="abbreviation">i<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i2"><span class="id" title="abbreviation">i<sub>2</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a>  <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="STLCExtendedRecords.typing_nonexample" class="idref" href="#STLCExtendedRecords.typing_nonexample"><span class="id" title="definition">typing_nonexample</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="T:95" class="idref" href="#T:95"><span class="id" title="binder">T</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a>  <a class="idref" href="Records.html#STLCExtendedRecords.i2"><span class="id" title="abbreviation">i<sub>2</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a><a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'nil'"><span class="id" title="notation">nil</span></a>   <a class="idref" href="Records.html#9117ef97be47c16687a336570867da4a"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i1"><span class="id" title="abbreviation">i<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.B"><span class="id" title="abbreviation">B</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a><a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#T:95"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="STLCExtendedRecords.typing_nonexample_2" class="idref" href="#STLCExtendedRecords.typing_nonexample_2"><span class="id" title="definition">typing_nonexample_2</span></a> : <span class="id" title="keyword">∀</span> <a id="y:96" class="idref" href="#y:96"><span class="id" title="binder">y</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#63a68285c81db8f9bc456233bb9ed181"><span class="id" title="notation">¬</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="T:97" class="idref" href="#T:97"><span class="id" title="binder">T</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#y:96"><span class="id" title="variable">y</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i1"><span class="id" title="abbreviation">i<sub>1</sub></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">:</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.A"><span class="id" title="abbreviation">A</span></a>  <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::x_':'_x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc_ty::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#d7100e6eff6251cc5929eb578deead9a"><span class="id" title="notation">)</span></a><a class="idref" href="Records.html#8e83a2cb3fb7bcc278eeca793b61ab<sub>67</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i1"><span class="id" title="abbreviation">i<sub>1</sub></span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">(</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i1"><span class="id" title="abbreviation">i<sub>1</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#y:96"><span class="id" title="variable">y</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.i2"><span class="id" title="abbreviation">i<sub>2</sub></span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <a class="idref" href="Records.html#y:96"><span class="id" title="variable">y</span></a> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::'nil'"><span class="id" title="notation">nil</span></a> <a class="idref" href="Records.html#6a63f178ee59cb86a0e9a58cfa031423"><span class="id" title="notation">)</span></a>  <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:97"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
</div>

<div class="doc">
<a id="lab375"></a><h2 class="section">Properties of Typing</h2>

<div class="paragraph"> </div>

 The proofs of progress and preservation for this system are
    essentially the same as for the pure simply typed lambda-calculus,
    but we need to add some technical lemmas involving records. 
</div>

<div class="doc">
<a id="lab376"></a><h3 class="section">Well-Formedness</h3>

</div>
<div class="code">

<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.wf_rcd_lookup" class="idref" href="#STLCExtendedRecords.wf_rcd_lookup"><span class="id" title="lemma">wf_rcd_lookup</span></a> : <span class="id" title="keyword">∀</span> <a id="i:98" class="idref" href="#i:98"><span class="id" title="binder">i</span></a> <a id="T:99" class="idref" href="#T:99"><span class="id" title="binder">T</span></a> <a id="Ti:100" class="idref" href="#Ti:100"><span class="id" title="binder">Ti</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.well_formed_ty"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T:99"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.Tlookup"><span class="id" title="definition">Tlookup</span></a> <a class="idref" href="Records.html#i:98"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#T:99"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Records.html#Ti:100"><span class="id" title="variable">Ti</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.well_formed_ty"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#Ti:100"><span class="id" title="variable">Ti</span></a>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">i</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">T</span>; <span class="id" title="tactic">intros</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Records.html#STLCExtendedRecords.Tlookup"><span class="id" title="definition">Tlookup</span></a> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<span class="id" title="definition">eqb_string</span> <span class="id" title="var">i</span> <span class="id" title="var">s</span>)...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">subst</span>... <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.step_preserves_record_tm" class="idref" href="#STLCExtendedRecords.step_preserves_record_tm"><span class="id" title="lemma">step_preserves_record_tm</span></a> : <span class="id" title="keyword">∀</span> <a id="tr:101" class="idref" href="#tr:101"><span class="id" title="binder">tr</span></a> <a id="tr':102" class="idref" href="#tr':102"><span class="id" title="binder">tr'</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.record_tm"><span class="id" title="inductive">record_tm</span></a> <a class="idref" href="Records.html#tr:101"><span class="id" title="variable">tr</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#tr:101"><span class="id" title="variable">tr</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#tr':102"><span class="id" title="variable">tr'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.record_tm"><span class="id" title="inductive">record_tm</span></a> <a class="idref" href="Records.html#tr':102"><span class="id" title="variable">tr'</span></a>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">tr</span> <span class="id" title="var">tr'</span> <span class="id" title="var">Hrt</span> <span class="id" title="var">Hstp</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">Hrt</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Hstp</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.has_type__wf" class="idref" href="#STLCExtendedRecords.has_type__wf"><span class="id" title="lemma">has_type__wf</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:103" class="idref" href="#Gamma:103"><span class="id" title="binder">Gamma</span></a> <a id="t:104" class="idref" href="#t:104"><span class="id" title="binder">t</span></a> <a id="T:105" class="idref" href="#T:105"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:103"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:104"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:105"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.well_formed_ty"><span class="id" title="inductive">well_formed_ty</span></a> <a class="idref" href="Records.html#T:105"><span class="id" title="variable">T</span></a>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">Htyp</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Htyp</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">IHHtyp1</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Proj&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Records.html#STLCExtendedRecords.wf_rcd_lookup"><span class="id" title="lemma">wf_rcd_lookup</span></a>...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab377"></a><h3 class="section">Field Lookup</h3>

<div class="paragraph"> </div>

 Lemma: If <span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">v</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode"><span class="id" title="var">Tlookup</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> returns <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">Ti</span></span>,
     then <span class="inlinecode"><span class="id" title="var">tlookup</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">v</span></span> returns <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">ti</span></span> for some term <span class="inlinecode"><span class="id" title="var">ti</span></span> such
     that <span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">ti</span></span> <span class="inlinecode">\<span class="id" title="keyword">in</span></span> <span class="inlinecode"><span class="id" title="var">Ti</span></span>.

<div class="paragraph"> </div>

    Proof: By induction on the typing derivation <span class="inlinecode"><span class="id" title="var">Htyp</span></span>.  Since
      <span class="inlinecode"><span class="id" title="var">Tlookup</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">Ti</span></span>, <span class="inlinecode"><span class="id" title="var">T</span></span> must be a record type, this and
      the fact that <span class="inlinecode"><span class="id" title="var">v</span></span> is a value eliminate most cases by inspection,
      leaving only the <span class="inlinecode"><span class="id" title="var">T_RCons</span></span> case.

<div class="paragraph"> </div>

      If the last step in the typing derivation is by <span class="inlinecode"><span class="id" title="var">T_RCons</span></span>, then
      <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span> and <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">RCons</span></span> <span class="inlinecode"><span class="id" title="var">i<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode"><span class="id" title="var">Tr</span></span> for some <span class="inlinecode"><span class="id" title="var">i<sub>0</sub></span></span>,
      <span class="inlinecode"><span class="id" title="var">t</span></span>, <span class="inlinecode"><span class="id" title="var">tr</span></span>, <span class="inlinecode"><span class="id" title="var">T</span></span> and <span class="inlinecode"><span class="id" title="var">Tr</span></span>.

<div class="paragraph"> </div>

      This leaves two possiblities to consider - either <span class="inlinecode"><span class="id" title="var">i<sub>0</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">i</span></span> or
      not.

<div class="paragraph"> </div>

<ul class="doclist">
<li> If <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">i<sub>0</sub></span></span>, then since <span class="inlinecode"><span class="id" title="var">Tlookup</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode">(<span class="id" title="var">RCons</span></span> <span class="inlinecode"><span class="id" title="var">i<sub>0</sub></span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode"><span class="id" title="var">Tr</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">Some</span></span>
        <span class="inlinecode"><span class="id" title="var">Ti</span></span> we have <span class="inlinecode"><span class="id" title="var">T</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">Ti</span></span>.  It follows that <span class="inlinecode"><span class="id" title="var">t</span></span> itself satisfies
        the theorem.

<div class="paragraph"> </div>


</li>
<li> On the other hand, suppose <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" title="var">i<sub>0</sub></span></span>.  Then
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">Tlookup</span> <span class="id" title="var">i</span> <span class="id" title="var">T</span> = <span class="id" title="var">Tlookup</span> <span class="id" title="var">i</span> <span class="id" title="var">Tr</span>
</span>        and
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">tlookup</span> <span class="id" title="var">i</span> <span class="id" title="var">t</span> = <span class="id" title="var">tlookup</span> <span class="id" title="var">i</span> <span class="id" title="var">tr</span>,
</span>        so the result follows from the induction hypothesis. <font size=-2>&#9744;</font>

</li>
</ul>

<div class="paragraph"> </div>

    Here is the formal statement:

</div>
<div class="code">

<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.lookup_field_in_value" class="idref" href="#STLCExtendedRecords.lookup_field_in_value"><span class="id" title="lemma">lookup_field_in_value</span></a> : <span class="id" title="keyword">∀</span> <a id="v:106" class="idref" href="#v:106"><span class="id" title="binder">v</span></a> <a id="T:107" class="idref" href="#T:107"><span class="id" title="binder">T</span></a> <a id="i:108" class="idref" href="#i:108"><span class="id" title="binder">i</span></a> <a id="Ti:109" class="idref" href="#Ti:109"><span class="id" title="binder">Ti</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#v:106"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#v:106"><span class="id" title="variable">v</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:107"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.Tlookup"><span class="id" title="definition">Tlookup</span></a> <a class="idref" href="Records.html#i:108"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#T:107"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Records.html#Ti:109"><span class="id" title="variable">Ti</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="ti:110" class="idref" href="#ti:110"><span class="id" title="binder">ti</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.tlookup"><span class="id" title="definition">tlookup</span></a> <a class="idref" href="Records.html#i:108"><span class="id" title="variable">i</span></a> <a class="idref" href="Records.html#v:106"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Records.html#ti:110"><span class="id" title="variable">ti</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#ti:110"><span class="id" title="variable">ti</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#Ti:109"><span class="id" title="variable">Ti</span></a>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">v</span> <span class="id" title="var">T</span> <span class="id" title="var">i</span> <span class="id" title="var">Ti</span> <span class="id" title="var">Hval</span> <span class="id" title="var">Htyp</span> <span class="id" title="var">Hget</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> <span class="id" title="definition">empty</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Htyp</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hget</span>. <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">destruct</span> (<span class="id" title="definition">eqb_string</span> <span class="id" title="var">i</span> <span class="id" title="var">i<sub>0</sub></span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;i&nbsp;is&nbsp;first&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">injection</span> <span class="id" title="var">Hget</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Hget</span>. <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">∃</span> <span class="id" title="var">t</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;get&nbsp;tail&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHtyp2</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">vi</span> [<span class="id" title="var">Hgeti</span> <span class="id" title="var">Htypi</span>] ]...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">Hval</span>... <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab378"></a><h3 class="section">Progress</h3>

</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="STLCExtendedRecords.progress" class="idref" href="#STLCExtendedRecords.progress"><span class="id" title="lemma">progress</span></a> : <span class="id" title="keyword">∀</span> <a id="t:111" class="idref" href="#t:111"><span class="id" title="binder">t</span></a> <a id="T:112" class="idref" href="#T:112"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:111"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:112"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#STLCExtendedRecords.value"><span class="id" title="inductive">value</span></a> <a class="idref" href="Records.html#t:111"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e<sub>25</sub>"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="t':113" class="idref" href="#t':113"><span class="id" title="binder">t'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="Records.html#t:111"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#t':113"><span class="id" title="variable">t'</span></a>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Theorem:&nbsp;Suppose&nbsp;empty&nbsp;&#x22A2;&nbsp;t&nbsp;:&nbsp;T.&nbsp;&nbsp;Then&nbsp;either<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;1.&nbsp;t&nbsp;is&nbsp;a&nbsp;value,&nbsp;or<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;2.&nbsp;t&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;t'&nbsp;for&nbsp;some&nbsp;t'.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Proof:&nbsp;By&nbsp;induction&nbsp;on&nbsp;the&nbsp;given&nbsp;typing&nbsp;derivation.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> <span class="id" title="definition">empty</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">HeqGamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Ht</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">HeqGamma</span>; <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;final&nbsp;rule&nbsp;in&nbsp;the&nbsp;given&nbsp;typing&nbsp;derivation&nbsp;cannot&nbsp;be<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">T_Var</span></span>,&nbsp;since&nbsp;it&nbsp;can&nbsp;never&nbsp;be&nbsp;the&nbsp;case&nbsp;that<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">T</span></span>&nbsp;(since&nbsp;the&nbsp;context&nbsp;is&nbsp;empty).&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;the&nbsp;<span class="inlinecode"><span class="id" title="var">T_Abs</span></span>&nbsp;rule&nbsp;was&nbsp;the&nbsp;last&nbsp;used,&nbsp;then<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">abs</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>11</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>12</sub></span></span>,&nbsp;which&nbsp;is&nbsp;a&nbsp;value.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;the&nbsp;last&nbsp;rule&nbsp;applied&nbsp;was&nbsp;T_App,&nbsp;then&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;and&nbsp;we&nbsp;know&nbsp;from&nbsp;the&nbsp;form&nbsp;of&nbsp;the&nbsp;rule&nbsp;that<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">T<sub>2</sub></span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">T<sub>1</sub></span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;By&nbsp;the&nbsp;induction&nbsp;hypothesis,&nbsp;each&nbsp;of&nbsp;t<sub>1</sub>&nbsp;and&nbsp;t<sub>2</sub>&nbsp;either&nbsp;is&nbsp;a&nbsp;value<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;or&nbsp;can&nbsp;take&nbsp;a&nbsp;step.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">right</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt1</span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt2</span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;both&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span>&nbsp;are&nbsp;values,&nbsp;then&nbsp;we&nbsp;know&nbsp;that<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">abs</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>11</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>12</sub></span></span>,&nbsp;since&nbsp;abstractions&nbsp;are&nbsp;the&nbsp;only<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;values&nbsp;that&nbsp;can&nbsp;have&nbsp;an&nbsp;arrow&nbsp;type.&nbsp;&nbsp;But<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode">(<span class="id" title="var">abs</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode"><span class="id" title="var">T<sub>11</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>12</sub></span>)</span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">[<span class="id" title="var">x</span>:=<span class="id" title="var">t<sub>2</sub></span>]<span class="id" title="var">t<sub>12</sub></span></span>&nbsp;by&nbsp;<span class="inlinecode"><span class="id" title="var">ST_AppAbs</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">∃</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><span class="id" title="var">x</span><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a><span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a><span class="id" title="var">t<sub>0</sub></span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="comment">(*&nbsp;t<sub>2</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span>&nbsp;is&nbsp;a&nbsp;value&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub>'</span></span>,&nbsp;then<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub>'</span></span>&nbsp;by&nbsp;<span class="inlinecode"><span class="id" title="var">ST_App2</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H<sub>0</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t<sub>2</sub>'</span> <span class="id" title="var">Hstp</span>]. <span class="id" title="tactic">∃</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub>'</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;t<sub>1</sub>&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Finally,&nbsp;If&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span>,&nbsp;then&nbsp;<span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>2</sub></span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;by&nbsp;<span class="inlinecode"><span class="id" title="var">ST_App1</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t<sub>1</sub>'</span> <span class="id" title="var">Hstp</span>]. <span class="id" title="tactic">∃</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">t<sub>1</sub>'</span> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Proj&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;the&nbsp;last&nbsp;rule&nbsp;in&nbsp;the&nbsp;given&nbsp;derivation&nbsp;is&nbsp;<span class="inlinecode"><span class="id" title="var">T_Proj</span></span>,&nbsp;then<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">rproj</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span>&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode">(<span class="id" title="var">TRcd</span></span> <span class="inlinecode"><span class="id" title="var">Tr</span>)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;By&nbsp;the&nbsp;IH,&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;either&nbsp;is&nbsp;a&nbsp;value&nbsp;or&nbsp;takes&nbsp;a&nbsp;step.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">right</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;rcd&nbsp;is&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;is&nbsp;a&nbsp;value,&nbsp;then&nbsp;we&nbsp;may&nbsp;use&nbsp;lemma<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">lookup_field_in_value</span></span>&nbsp;to&nbsp;show&nbsp;<span class="inlinecode"><span class="id" title="var">tlookup</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">ti</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;for&nbsp;some&nbsp;<span class="inlinecode"><span class="id" title="var">ti</span></span>&nbsp;which&nbsp;gives&nbsp;us&nbsp;<span class="inlinecode"><span class="id" title="var">rproj</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">ti</span></span>&nbsp;by<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">ST_ProjRcd</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="Records.html#STLCExtendedRecords.lookup_field_in_value"><span class="id" title="lemma">lookup_field_in_value</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H<sub>0</sub></span> <span class="id" title="var">Ht</span> <span class="id" title="var">H</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">as</span> [<span class="id" title="var">ti</span> [<span class="id" title="var">Hlkup</span> <span class="id" title="var">_</span>] ].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">∃</span> <span class="id" title="var">ti</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;rcd_steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;On&nbsp;the&nbsp;other&nbsp;hand,&nbsp;if&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span>,&nbsp;then<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">rproj</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">rproj</span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span>&nbsp;by&nbsp;<span class="inlinecode"><span class="id" title="var">ST_Proj1</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">H<sub>0</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t'</span> <span class="id" title="var">Hstp</span>]. <span class="id" title="tactic">∃</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">t'</span> <a class="idref" href="Records.html#STLCExtendedRecords.:stlc::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <span class="id" title="var">i</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RNil&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;the&nbsp;last&nbsp;rule&nbsp;in&nbsp;the&nbsp;given&nbsp;derivation&nbsp;is&nbsp;<span class="inlinecode"><span class="id" title="var">T_RNil</span></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;then&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">trnil</span></span>,&nbsp;which&nbsp;is&nbsp;a&nbsp;value.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;the&nbsp;last&nbsp;rule&nbsp;is&nbsp;<span class="inlinecode"><span class="id" title="var">T_RCons</span></span>,&nbsp;then&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span>&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">T</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">tr</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">Tr</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;By&nbsp;the&nbsp;IH,&nbsp;each&nbsp;of&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">tr</span></span>&nbsp;either&nbsp;is&nbsp;a&nbsp;value&nbsp;or&nbsp;can<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;take&nbsp;a&nbsp;step.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt1</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;head&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">IHHt2</span>; <span class="id" title="tactic">try</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="comment">(*&nbsp;tail&nbsp;is&nbsp;a&nbsp;value&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">tr</span></span>&nbsp;are&nbsp;both&nbsp;values,&nbsp;then&nbsp;<span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;is&nbsp;a&nbsp;value&nbsp;as&nbsp;well.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">left</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;× <span class="comment">(*&nbsp;tail&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;is&nbsp;a&nbsp;value&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">tr</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">tr'</span></span>,&nbsp;then<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">tr'</span></span>&nbsp;by<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">ST_Rcd_Tail</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">right</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">H<sub>2</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">tr'</span> <span class="id" title="var">Hstp</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">∃</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">i</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <span class="id" title="var">t</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <span class="id" title="var">tr'</span><a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;head&nbsp;steps&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span>,&nbsp;then<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;by&nbsp;<span class="inlinecode"><span class="id" title="var">ST_Rcd_Head</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">right</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">t'</span> <span class="id" title="var">Hstp</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">∃</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">i</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">:=</span></a> <span class="id" title="var">t'</span> <a class="idref" href="Records.html#81f41eb8d6c9df1b60000d935db1438c"><span class="id" title="notation">::</span></a> <span class="id" title="var">tr</span> <a class="idref" href="Records.html#578583e5bab5b75c1f745f27b2fa3362"><span class="id" title="notation">}&gt;</span></a>... <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab379"></a><h2 class="section">Weakening</h2>

<div class="paragraph"> </div>

 The weakening lemma is proved as in pure STLC. 
</div>
<div class="code">

<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.weakening" class="idref" href="#STLCExtendedRecords.weakening"><span class="id" title="lemma">weakening</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:114" class="idref" href="#Gamma:114"><span class="id" title="binder">Gamma</span></a> <a id="Gamma':115" class="idref" href="#Gamma':115"><span class="id" title="binder">Gamma'</span></a> <a id="t:116" class="idref" href="#t:116"><span class="id" title="binder">t</span></a> <a id="T:117" class="idref" href="#T:117"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">inclusion</span> <a class="idref" href="Records.html#Gamma:114"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#Gamma':115"><span class="id" title="variable">Gamma'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:114"><span class="id" title="variable">Gamma</span></a>  <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:116"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:117"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma':115"><span class="id" title="variable">Gamma'</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:116"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:117"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">Gamma'</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">H</span> <span class="id" title="var">Ht</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma'</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Ht</span>; <span class="id" title="tactic">eauto</span> <span class="id" title="keyword">using</span> <span class="id" title="lemma">inclusion_update</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.weakening_empty" class="idref" href="#STLCExtendedRecords.weakening_empty"><span class="id" title="lemma">weakening_empty</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:118" class="idref" href="#Gamma:118"><span class="id" title="binder">Gamma</span></a> <a id="t:119" class="idref" href="#t:119"><span class="id" title="binder">t</span></a> <a id="T:120" class="idref" href="#T:120"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:119"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:120"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:118"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:119"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:120"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Records.html#STLCExtendedRecords.weakening"><span class="id" title="lemma">weakening</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">discriminate</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab380"></a><h3 class="section">Preservation</h3>

<div class="paragraph"> </div>

 As before, we prove the substitution lemma by induction
    on the term t. The only new case (compared to the proof in
    StlcProp.v) is the case of rcons. For this case, we must do a little
    extra work to show that substituting into a term doesn't change
    whetherit is a record term. 
</div>
<div class="code">

<span class="id" title="keyword">Lemma</span> <a id="STLCExtendedRecords.substitution_preserves_typing" class="idref" href="#STLCExtendedRecords.substitution_preserves_typing"><span class="id" title="lemma">substitution_preserves_typing</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:121" class="idref" href="#Gamma:121"><span class="id" title="binder">Gamma</span></a> <a id="x:122" class="idref" href="#x:122"><span class="id" title="binder">x</span></a> <a id="U:123" class="idref" href="#U:123"><span class="id" title="binder">U</span></a> <a id="t:124" class="idref" href="#t:124"><span class="id" title="binder">t</span></a> <a id="v:125" class="idref" href="#v:125"><span class="id" title="binder">v</span></a> <a id="T:126" class="idref" href="#T:126"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Records.html#x:122"><span class="id" title="variable">x</span></a> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="Records.html#U:123"><span class="id" title="variable">U</span></a> <span class="id" title="notation">;</span> <a class="idref" href="Records.html#Gamma:121"><span class="id" title="variable">Gamma</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:124"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:126"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#v:125"><span class="id" title="variable">v</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#U:123"><span class="id" title="variable">U</span></a>   <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#Gamma:121"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Records.html#x:122"><span class="id" title="variable">x</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">:=</span></a><a class="idref" href="Records.html#v:125"><span class="id" title="variable">v</span></a><a class="idref" href="Records.html#6b3bab402afeb111cd472fd09a3b5ea<sub>9</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="Records.html#t:124"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:126"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">x</span> <span class="id" title="var">U</span> <span class="id" title="var">t</span> <span class="id" title="var">v</span> <span class="id" title="var">T</span> <span class="id" title="var">Ht</span> <span class="id" title="var">Hv</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">t</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">T</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">H</span>;<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;in&nbsp;each&nbsp;case,&nbsp;we'll&nbsp;want&nbsp;to&nbsp;get&nbsp;at&nbsp;the&nbsp;derivation&nbsp;of&nbsp;H&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">H</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;var&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">y</span>. <span class="id" title="tactic">destruct</span> (<span class="id" title="axiom">eqb_stringP</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>); <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x=y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_eq</span> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">injection</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>1</sub></span>; <span class="id" title="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Records.html#STLCExtendedRecords.weakening_empty"><span class="id" title="lemma">weakening_empty</span></a>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x&lt;&gt;y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Records.html#STLCExtendedRecords.T_Var"><span class="id" title="constructor">T_Var</span></a>. <span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_neq</span> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>1</sub></span>; <span class="id" title="tactic">auto</span>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">y</span>, <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<span class="id" title="axiom">eqb_stringP</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>); <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">apply</span> <a class="idref" href="Records.html#STLCExtendedRecords.T_Abs"><span class="id" title="constructor">T_Abs</span></a>; <span class="id" title="tactic">try</span> <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x=y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_shadow</span> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>5</sub></span>. <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;x&lt;&gt;y&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHt</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="lemma">update_permute</span>; <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;rcons&nbsp;*)</span>   <span class="comment">(*&nbsp;&lt;===&nbsp;only&nbsp;new&nbsp;case&nbsp;compared&nbsp;to&nbsp;pure&nbsp;STLC&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Records.html#STLCExtendedRecords.T_RCons"><span class="id" title="constructor">T_RCons</span></a>; <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>7</sub></span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">auto</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="STLCExtendedRecords.preservation" class="idref" href="#STLCExtendedRecords.preservation"><span class="id" title="lemma">preservation</span></a> : <span class="id" title="keyword">∀</span> <a id="t:127" class="idref" href="#t:127"><span class="id" title="binder">t</span></a> <a id="t':128" class="idref" href="#t':128"><span class="id" title="binder">t'</span></a> <a id="T:129" class="idref" href="#T:129"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t:127"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:129"><span class="id" title="variable">T</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Records.html#t:127"><span class="id" title="variable">t</span></a> <a class="idref" href="Records.html#STLCExtendedRecords.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Records.html#t':128"><span class="id" title="variable">t'</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<span class="id" title="definition">empty</span> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">&#x22A2;</span></a> <a class="idref" href="Records.html#t':128"><span class="id" title="variable">t'</span></a> <a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">\</span></a><a class="idref" href="Records.html#308929c34b30aea3b8569a5808139a<sub>21</sub>"><span class="id" title="notation">in</span></a> <a class="idref" href="Records.html#T:129"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">t'</span> <span class="id" title="var">T</span> <span class="id" title="var">HT</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">t'</span>.<br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> <span class="id" title="definition">empty</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">HT</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">t'</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> <span class="id" title="tactic">solve</span> [<span class="id" title="tactic">inversion</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">auto</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ST_AppAbs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Records.html#STLCExtendedRecords.substitution_preserves_typing"><span class="id" title="lemma">substitution_preserves_typing</span></a> <span class="id" title="keyword">with</span> <span class="id" title="var">T<sub>1</sub></span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">HT<sub>1</sub></span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Proj&nbsp;*)</span> <span class="comment">(*&nbsp;&lt;===&nbsp;new&nbsp;case&nbsp;compared&nbsp;to&nbsp;pure&nbsp;STLC&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;the&nbsp;last&nbsp;rule&nbsp;was&nbsp;<span class="inlinecode"><span class="id" title="var">T_Proj</span></span>,&nbsp;then&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">rproj</span></span> <span class="inlinecode"><span class="id" title="var">t<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">i</span></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Two&nbsp;rules&nbsp;could&nbsp;have&nbsp;caused&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">t'</span></span>:&nbsp;<span class="inlinecode"><span class="id" title="var">T_Proj1</span></span>&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">T_ProjRcd</span></span>.&nbsp;&nbsp;The&nbsp;typing&nbsp;of&nbsp;<span class="inlinecode"><span class="id" title="var">t'</span></span>&nbsp;follows&nbsp;from&nbsp;the&nbsp;IH<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in&nbsp;the&nbsp;former&nbsp;case,&nbsp;so&nbsp;we&nbsp;only&nbsp;consider&nbsp;<span class="inlinecode"><span class="id" title="var">T_ProjRcd</span></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Here&nbsp;we&nbsp;have&nbsp;that&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;is&nbsp;a&nbsp;record&nbsp;value.&nbsp;&nbsp;Since&nbsp;rule<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">T_Proj</span></span>&nbsp;was&nbsp;used,&nbsp;we&nbsp;know&nbsp;<span class="inlinecode"><span class="id" title="var">empty</span></span> <span class="inlinecode">&#x22A2;</span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">\<span class="id" title="keyword">in</span></span> <span class="inlinecode"><span class="id" title="var">Tr</span></span>&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">Tlookup</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">Tr</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">Ti</span></span>&nbsp;for&nbsp;some&nbsp;<span class="inlinecode"><span class="id" title="var">i</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">Tr</span></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;We&nbsp;may&nbsp;therefore&nbsp;apply&nbsp;lemma&nbsp;<span class="inlinecode"><span class="id" title="var">lookup_field_in_value</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;to&nbsp;find&nbsp;the&nbsp;record&nbsp;element&nbsp;this&nbsp;projection&nbsp;steps&nbsp;to.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="Records.html#STLCExtendedRecords.lookup_field_in_value"><span class="id" title="lemma">lookup_field_in_value</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H<sub>2</sub></span> <span class="id" title="var">HT</span> <span class="id" title="var">H</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">as</span> [<span class="id" title="var">vi</span> [<span class="id" title="var">Hget</span> <span class="id" title="var">Htyp</span>] ].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>4</sub></span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hget</span>. <span class="id" title="tactic">injection</span> <span class="id" title="var">Hget</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Hget</span>. <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_RCons&nbsp;*)</span> <span class="comment">(*&nbsp;&lt;===&nbsp;new&nbsp;case&nbsp;compared&nbsp;to&nbsp;pure&nbsp;STLC&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;If&nbsp;the&nbsp;last&nbsp;rule&nbsp;was&nbsp;<span class="inlinecode"><span class="id" title="var">T_RCons</span></span>,&nbsp;then&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">rcons</span></span> <span class="inlinecode"><span class="id" title="var">i</span></span> <span class="inlinecode"><span class="id" title="var">t</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;for&nbsp;some&nbsp;<span class="inlinecode"><span class="id" title="var">i</span></span>,&nbsp;<span class="inlinecode"><span class="id" title="var">t</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">tr</span></span>&nbsp;such&nbsp;that&nbsp;<span class="inlinecode"><span class="id" title="var">record_tm</span></span> <span class="inlinecode"><span class="id" title="var">tr</span></span>.&nbsp;&nbsp;If<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;the&nbsp;step&nbsp;is&nbsp;by&nbsp;<span class="inlinecode"><span class="id" title="var">ST_Rcd_Head</span></span>,&nbsp;the&nbsp;result&nbsp;is&nbsp;immediate&nbsp;by<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;the&nbsp;IH.&nbsp;&nbsp;If&nbsp;the&nbsp;step&nbsp;is&nbsp;by&nbsp;<span class="inlinecode"><span class="id" title="var">ST_Rcd_Tail</span></span>,&nbsp;<span class="inlinecode"><span class="id" title="var">tr</span></span> <span class="inlinecode"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" title="var">tr<sub>2</sub>'</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;for&nbsp;some&nbsp;<span class="inlinecode"><span class="id" title="var">tr<sub>2</sub>'</span></span>&nbsp;and&nbsp;we&nbsp;must&nbsp;also&nbsp;use&nbsp;lemma&nbsp;<span class="inlinecode"><span class="id" title="var">step_preserves_record_tm</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;to&nbsp;show&nbsp;<span class="inlinecode"><span class="id" title="var">record_tm</span></span> <span class="inlinecode"><span class="id" title="var">tr<sub>2</sub>'</span></span>.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">HE</span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Records.html#STLCExtendedRecords.T_RCons"><span class="id" title="constructor">T_RCons</span></a>... <span class="id" title="tactic">eapply</span> <a class="idref" href="Records.html#STLCExtendedRecords.step_preserves_record_tm"><span class="id" title="lemma">step_preserves_record_tm</span></a>...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<span class="id" title="keyword">End</span> <a class="idref" href="Records.html#STLCExtendedRecords"><span class="id" title="module">STLCExtendedRecords</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2021-08-11&nbsp;15:11&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>